Nuprl Definition : existse-between2 11,40

e[e1,e2].P(e) == e:es-E(es). ((es-le(ese1e es-le(esee2)) c P(e)) 
latex



clarification:

existse-between2(es;e1;e2;e.P(e))
== e:es-E(es). ((es-le(ese1e es-le(esee2)) c P(e)) 
latex


Definitionsx:AB(x), es-E(es), A c B, P  Q, es-le(esee')
FDL editor aliasesexistse-between2

origin